{-
 This file is part of the Clafer to Alloy Translator (clafer2alloy).

 Copyright (C) 2010 Kacper Bak <http://gsd.uwaterloo.ca/kbak>

 clafer2alloy is free software: you can redistribute it and/or modify
 it under the terms of the GNU Lesser General Public License as published by
 the Free Software Foundation, either version 3 of the License, or
 (at your option) any later version.

 clafer2alloy is distributed in the hope that it will be useful,
 but WITHOUT ANY WARRANTY; without even the implied warranty of
 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 GNU Lesser General Public License for more details.

 You should have received a copy of the GNU Lesser General Public License
 along with clafer2alloy. (See files COPYING and COPYING.LESSER.)  If not,
 see <http://www.gnu.org/licenses/>.
-}
module AlloyCode where

import Data.Char

header = unlines
    [ "pred show {}"
    , "run  show for 1"
    , ""
{-    , concat [ "abstract sig ", baseClafer, " {" ++ parent ++ " : one ",
               baseClafer, "}"]
    , concat [ "lone sig ", strType, " extends ", baseClafer, " {", valField
             , " : Int}", "{", parent, " = ", this, "}"]
    , concat [ "lone sig ", intType, " extends ", baseClafer, " {", valField
             , " : Int}", "{", parent, " = ", this, "}"] 
    , concat ["fun ", children, "(p : ",  baseClafer, ") : set ", baseClafer,
              "{p.~", parent, " - p}"] -}
    , ""]

no   = "no"
one  = "one"
lone = "lone"
some = "some"
set  = "set"
disj = "disj"

parent = "parent"

this = "this"

baseClafer = "clafer"

subclafers = "subclafers"

children = "children"

attrField = "ref"

valField = "val"

strType = "string"

intType = "integer"

noAttr = "no   " ++ attrField

noSubclafers = "no   " ++ subclafers

noParent = "no   " ++ parent

claferDecl name predecessors (moduleName, super) =
  featureDef name predecessors ++ extends (maybe "" id moduleName) super

featureDef = ((((++) "sig ").(mkName "_" id)).).(:)

extends _ "clafer" = ""
extends mod super = " extends " ++ mod ++ super

mkClaferDef decl rels constraints = unlines
  [ decl
  , showSet "\n, " rels
  , showSet "\n  " constraints]

mkFact xs = concat ["fact ", mkSet xs, "\n"]

showSet delim xs = showSet' delim $ filter (not.null) xs

showSet' _ []     = "{}"
showSet' delim xs = mkSet $ foldWith delim xs

mkSet xs = "{ " ++ xs ++ " }"

foldWith = (foldl1.) concWith

mkAttribute = relIn attrField

relIn rel set = concat [rel, " in ", set]
    
noAbs name = noAbs' name ++ "\n"

noAbs' name = featureDef name' [] ++ extends "" name ++ " {} " ++
             showSet "" ["no " ++ name']
  where
  name' = "abs" ++ name

parentIs = parent ++ " = "

-- hierarchy constraint
hConst [] _ = ""
hConst predecessors name =
  parentIs ++ "(" ++ mkName "_" id predecessors ++ " <: " ++ name ++ ").this"

less = concWith " <= "

count = (++) "#"

mkName inter = (((foldl1 (concWith inter)).reverse).).map

concWith = ((++).).flip (++)

letSubclafers = "let " ++ subclafers ++ " = this.children |" 

--- extra
mkSubName hNames = mkName "_" id (subclafers : hNames)